postulate
  @flat A : Set
